T:Type, as:(T List), f,g:(T).
(priority-select(f; g; as) = (inr  )  (?))
 l_all(as; T; a.((((f(a))))  (((g(a)))))) 

latex

Definitions	(x  l), {x:A| B(x)} , x.A(x), t  T, s = t, l_all(L; T; x.P(x)), x:A  B(x), A, b, f(a), Type, P  Q, prop{i:l}, x. t(x), x:AB(x), x:A. B(x), type List, P  Q, P  Q, P  Q, ||as||, a < b, False, A  B, lelt(i; j; k), , int_seg(i; j), void, l[i], #$n, , , left + right, decision, inr x , priority-select(f; g; as), Unit, ff, inl x , n + m, x:A. B(x), tt, , grp_car(g), subtype(S; T), A c B
Lemmas	select member, le wf, priority-select-property, iff functionality wrt iff, iff wf, rev implies wf, unit wf, priority-select wf, bool wf, it wf, int seg wf, length wf1, select wf, l all wf, assert wf, not wf, l all wf2, l member wf